YES 1.942 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((intersect :: (Eq a, Eq b) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)]) :: (Eq b, Eq a) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (\vv2 ->
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []
) xs


module Maybe where
  import qualified List
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\vv2
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []

is transformed to
intersectBy0 eq ys vv2 = 
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((intersect :: (Eq a, Eq b) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)]) :: (Eq b, Eq a) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case vv2 of
 x → if any (eq xys then x : [] else []
 _ → []

is transformed to
intersectBy00 eq ys x = if any (eq xys then x : [] else []
intersectBy00 eq ys _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((intersect :: (Eq b, Eq a) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)]) :: (Eq b, Eq a) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x  if any (eq x) ys then x : [] else []
intersectBy00 eq ys _ []


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if any (eq xys then x : [] else []

is transformed to
intersectBy000 x True = x : []
intersectBy000 x False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((intersect :: (Eq a, Eq b) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)]) :: (Eq b, Eq a) => [(a,b)]  ->  [(a,b)]  ->  [(a,b)])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys _ []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((intersect :: (Eq b, Eq a) => [(b,a)]  ->  [(b,a)]  ->  [(b,a)]) :: (Eq a, Eq b) => [(b,a)]  ->  [(b,a)]  ->  [(b,a)])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ Narrow

mainModule List
  (intersect :: (Eq a, Eq b) => [(b,a)]  ->  [(b,a)]  ->  [(b,a)])

module List where
  import qualified Maybe
import qualified Prelude

  intersect :: Eq a => [a ->  [a ->  [a]
intersect intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool ->  [a ->  [a ->  [a]
intersectBy eq xs ys concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 intersectBy00 eq ys vv2

  
intersectBy00 eq ys x intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw []

  
intersectBy000 x True x : []
intersectBy000 x False []


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xx4300), Succ(xx4000000)) → new_primPlusNat(xx4300, xx4000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xx300000), Succ(xx400000)) → new_primMulNat(xx300000, Succ(xx400000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xx30000), Succ(xx40000)) → new_primEqNat(xx30000, xx40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(Right(xx3000), Right(xx4000), he, app(ty_Maybe, baf)) → new_esEs3(xx3000, xx4000, baf)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, cd, app(app(ty_Either, ff), fg)) → new_esEs1(xx3002, xx4002, ff, fg)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_Maybe, df), cd, ce) → new_esEs3(xx3000, xx4000, df)
new_esEs1(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ge), gf), gg), gd) → new_esEs0(xx3000, xx4000, ge, gf, gg)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), bca, app(app(ty_@2, bch), bda)) → new_esEs2(xx3001, xx4001, bch, bda)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, app(app(ty_@2, ef), eg), ce) → new_esEs2(xx3001, xx4001, ef, eg)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_Either, db), dc), cd, ce) → new_esEs1(xx3000, xx4000, db, dc)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_Maybe, bbh), bah) → new_esEs3(xx3000, xx4000, bbh)
new_esEs1(Right(xx3000), Right(xx4000), he, app(app(app(ty_@3, hg), hh), baa)) → new_esEs0(xx3000, xx4000, hg, hh, baa)
new_esEs(:(xx3000, xx3001), :(xx4000, xx4001), app(app(ty_@2, bg), bh)) → new_esEs2(xx3000, xx4000, bg, bh)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_@2, bbf), bbg), bah) → new_esEs2(xx3000, xx4000, bbf, bbg)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), bca, app(ty_Maybe, bdb)) → new_esEs3(xx3001, xx4001, bdb)
new_esEs1(Left(xx3000), Left(xx4000), app(app(ty_Either, gh), ha), gd) → new_esEs1(xx3000, xx4000, gh, ha)
new_esEs1(Right(xx3000), Right(xx4000), he, app(app(ty_Either, bab), bac)) → new_esEs1(xx3000, xx4000, bab, bac)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, app(app(app(ty_@3, ea), eb), ec), ce) → new_esEs0(xx3001, xx4001, ea, eb, ec)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_@2, dd), de), cd, ce) → new_esEs2(xx3000, xx4000, dd, de)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, cd, app(ty_[], fa)) → new_esEs(xx3002, xx4002, fa)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, app(app(ty_Either, ed), ee), ce) → new_esEs1(xx3001, xx4001, ed, ee)
new_esEs1(Left(xx3000), Left(xx4000), app(app(ty_@2, hb), hc), gd) → new_esEs2(xx3000, xx4000, hb, hc)
new_esEs3(Just(xx3000), Just(xx4000), app(app(ty_@2, bea), beb)) → new_esEs2(xx3000, xx4000, bea, beb)
new_esEs3(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs0(xx3000, xx4000, bdd, bde, bdf)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, app(ty_Maybe, eh), ce) → new_esEs3(xx3001, xx4001, eh)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, cd, app(ty_Maybe, gb)) → new_esEs3(xx3002, xx4002, gb)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), bca, app(app(ty_Either, bcf), bcg)) → new_esEs1(xx3001, xx4001, bcf, bcg)
new_esEs3(Just(xx3000), Just(xx4000), app(ty_[], bdc)) → new_esEs(xx3000, xx4000, bdc)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, cd, app(app(ty_@2, fh), ga)) → new_esEs2(xx3002, xx4002, fh, ga)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_[], cc), cd, ce) → new_esEs(xx3000, xx4000, cc)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), bca, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xx3001, xx4001, bcc, bcd, bce)
new_esEs(:(xx3000, xx3001), :(xx4000, xx4001), cb) → new_esEs(xx3001, xx4001, cb)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), bca, app(ty_[], bcb)) → new_esEs(xx3001, xx4001, bcb)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, cd, app(app(app(ty_@3, fb), fc), fd)) → new_esEs0(xx3002, xx4002, fb, fc, fd)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), dg, app(ty_[], dh), ce) → new_esEs(xx3001, xx4001, dh)
new_esEs1(Right(xx3000), Right(xx4000), he, app(app(ty_@2, bad), bae)) → new_esEs2(xx3000, xx4000, bad, bae)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(app(ty_@3, bba), bbb), bbc), bah) → new_esEs0(xx3000, xx4000, bba, bbb, bbc)
new_esEs3(Just(xx3000), Just(xx4000), app(ty_Maybe, bec)) → new_esEs3(xx3000, xx4000, bec)
new_esEs(:(xx3000, xx3001), :(xx4000, xx4001), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(xx3000, xx4000, bb, bc, bd)
new_esEs(:(xx3000, xx3001), :(xx4000, xx4001), app(ty_Maybe, ca)) → new_esEs3(xx3000, xx4000, ca)
new_esEs1(Left(xx3000), Left(xx4000), app(ty_Maybe, hd), gd) → new_esEs3(xx3000, xx4000, hd)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_[], bag), bah) → new_esEs(xx3000, xx4000, bag)
new_esEs(:(xx3000, xx3001), :(xx4000, xx4001), app(app(ty_Either, be), bf)) → new_esEs1(xx3000, xx4000, be, bf)
new_esEs1(Right(xx3000), Right(xx4000), he, app(ty_[], hf)) → new_esEs(xx3000, xx4000, hf)
new_esEs1(Left(xx3000), Left(xx4000), app(ty_[], gc), gd) → new_esEs(xx3000, xx4000, gc)
new_esEs3(Just(xx3000), Just(xx4000), app(app(ty_Either, bdg), bdh)) → new_esEs1(xx3000, xx4000, bdg, bdh)
new_esEs2(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_Either, bbd), bbe), bah) → new_esEs1(xx3000, xx4000, bbd, bbe)
new_esEs(:(xx3000, xx3001), :(xx4000, xx4001), app(ty_[], ba)) → new_esEs(xx3000, xx4000, ba)
new_esEs0(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(app(ty_@3, cf), cg), da), cd, ce) → new_esEs0(xx3000, xx4000, cf, cg, da)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(xx25, xx26, False, xx28, xx29, ba, bb) → new_psPs0(@2(xx25, xx26), xx28, xx29, ba, bb)
new_psPs0(@2(xx300, xx301), :(@2(xx400, xx401), xx41), xx5, bc, bd) → new_psPs(xx300, xx301, new_asAs(new_esEs4(xx300, xx400, bc), new_esEs5(xx301, xx401, bd)), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs15(Just(xx3000), Just(xx4000), app(app(ty_Either, bgg), bgh)) → new_esEs13(xx3000, xx4000, bgg, bgh)
new_primPlusNat1(Succ(xx4300), Succ(xx4000000)) → Succ(Succ(new_primPlusNat1(xx4300, xx4000000)))
new_esEs27(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bdh), bea), beb)) → new_esEs12(xx3000, xx4000, bdh, bea, beb)
new_esEs4(xx300, xx400, ty_@0) → new_esEs16(xx300, xx400)
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_esEs20(xx3000, xx4000, ty_@0) → new_esEs16(xx3000, xx4000)
new_esEs15(Just(xx3000), Just(xx4000), app(ty_Ratio, bhd)) → new_esEs18(xx3000, xx4000, bhd)
new_esEs27(xx3001, xx4001, app(ty_Ratio, bgb)) → new_esEs18(xx3001, xx4001, bgb)
new_esEs22(xx3002, xx4002, ty_Ordering) → new_esEs7(xx3002, xx4002)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs11(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs13(Left(xx3000), Left(xx4000), ty_Bool, cb) → new_esEs6(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs11(xx3000, xx4000)
new_esEs15(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs11(xx3000, xx4000)
new_esEs13(Left(xx3000), Left(xx4000), app(app(ty_Either, hc), hd), cb) → new_esEs13(xx3000, xx4000, hc, hd)
new_esEs23(xx3000, xx4000, app(app(ty_Either, bbg), bbh)) → new_esEs13(xx3000, xx4000, bbg, bbh)
new_esEs20(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs22(xx3002, xx4002, ty_@0) → new_esEs16(xx3002, xx4002)
new_esEs23(xx3000, xx4000, ty_Float) → new_esEs17(xx3000, xx4000)
new_esEs20(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs17(xx3000, xx4000)
new_esEs5(xx301, xx401, app(ty_[], bce)) → new_esEs10(xx301, xx401, bce)
new_esEs7(LT, GT) → False
new_esEs7(GT, LT) → False
new_primMulNat0(Zero, Zero) → Zero
new_esEs15(Just(xx3000), Just(xx4000), ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs5(xx301, xx401, app(ty_Ratio, bdf)) → new_esEs18(xx301, xx401, bdf)
new_esEs4(xx300, xx400, app(ty_Ratio, cf)) → new_esEs18(xx300, xx400, cf)
new_esEs26(xx3000, xx4000, app(ty_Maybe, beg)) → new_esEs15(xx3000, xx4000, beg)
new_esEs13(Right(xx3000), Right(xx4000), ca, app(app(ty_@2, bag), bah)) → new_esEs14(xx3000, xx4000, bag, bah)
new_esEs21(xx3001, xx4001, ty_Ordering) → new_esEs7(xx3001, xx4001)
new_esEs23(xx3000, xx4000, app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs12(xx3000, xx4000, bbd, bbe, bbf)
new_esEs20(xx3000, xx4000, app(app(ty_@2, df), dg)) → new_esEs14(xx3000, xx4000, df, dg)
new_esEs21(xx3001, xx4001, app(ty_[], eb)) → new_esEs10(xx3001, xx4001, eb)
new_primPlusNat0(Zero, xx400000) → Succ(xx400000)
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Integer) → new_esEs11(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_Ratio, beh)) → new_esEs18(xx3000, xx4000, beh)
new_esEs13(Left(xx3000), Left(xx4000), ty_Char, cb) → new_esEs19(xx3000, xx4000)
new_esEs15(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs6(xx3000, xx4000)
new_esEs20(xx3000, xx4000, app(app(app(ty_@3, da), db), dc)) → new_esEs12(xx3000, xx4000, da, db, dc)
new_esEs12(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), bf, bg, bh) → new_asAs(new_esEs20(xx3000, xx4000, bf), new_asAs(new_esEs21(xx3001, xx4001, bg), new_esEs22(xx3002, xx4002, bh)))
new_sr(Neg(xx30000), Pos(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_sr(Pos(xx30000), Neg(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_esEs22(xx3002, xx4002, ty_Integer) → new_esEs11(xx3002, xx4002)
new_esEs15(Just(xx3000), Just(xx4000), ty_Float) → new_esEs17(xx3000, xx4000)
new_esEs23(xx3000, xx4000, app(ty_[], bbc)) → new_esEs10(xx3000, xx4000, bbc)
new_esEs26(xx3000, xx4000, app(ty_[], bdg)) → new_esEs10(xx3000, xx4000, bdg)
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs11(xx3001, xx4001)
new_esEs7(LT, LT) → True
new_esEs20(xx3000, xx4000, app(app(ty_Either, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs15(Just(xx3000), Just(xx4000), app(ty_[], bgc)) → new_esEs10(xx3000, xx4000, bgc)
new_esEs24(xx3000, xx4000, ty_Integer) → new_esEs11(xx3000, xx4000)
new_esEs22(xx3002, xx4002, app(app(ty_Either, ga), gb)) → new_esEs13(xx3002, xx4002, ga, gb)
new_esEs23(xx3000, xx4000, app(ty_Maybe, bcc)) → new_esEs15(xx3000, xx4000, bcc)
new_esEs4(xx300, xx400, ty_Float) → new_esEs17(xx300, xx400)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs6(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs7(xx300, xx400)
new_esEs13(Left(xx3000), Left(xx4000), ty_Ordering, cb) → new_esEs7(xx3000, xx4000)
new_esEs22(xx3002, xx4002, app(ty_Ratio, gf)) → new_esEs18(xx3002, xx4002, gf)
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Succ(xx30000), Zero) → False
new_esEs21(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs22(xx3002, xx4002, ty_Float) → new_esEs17(xx3002, xx4002)
new_esEs15(Just(xx3000), Just(xx4000), ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs17(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs22(xx3002, xx4002, app(app(ty_@2, gc), gd)) → new_esEs14(xx3002, xx4002, gc, gd)
new_esEs20(xx3000, xx4000, app(ty_[], cg)) → new_esEs10(xx3000, xx4000, cg)
new_esEs27(xx3001, xx4001, app(app(ty_Either, bfe), bff)) → new_esEs13(xx3001, xx4001, bfe, bff)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(xx3000, xx4000, app(ty_Ratio, bcd)) → new_esEs18(xx3000, xx4000, bcd)
new_esEs13(Left(xx3000), Left(xx4000), app(app(ty_@2, he), hf), cb) → new_esEs14(xx3000, xx4000, he, hf)
new_esEs20(xx3000, xx4000, ty_Bool) → new_esEs6(xx3000, xx4000)
new_esEs21(xx3001, xx4001, app(app(ty_@2, eh), fa)) → new_esEs14(xx3001, xx4001, eh, fa)
new_esEs27(xx3001, xx4001, ty_@0) → new_esEs16(xx3001, xx4001)
new_esEs13(Left(xx3000), Left(xx4000), ty_Double, cb) → new_esEs8(xx3000, xx4000)
new_esEs22(xx3002, xx4002, ty_Int) → new_esEs9(xx3002, xx4002)
new_esEs4(xx300, xx400, app(ty_[], be)) → new_esEs10(xx300, xx400, be)
new_esEs21(xx3001, xx4001, app(app(app(ty_@3, ec), ed), ee)) → new_esEs12(xx3001, xx4001, ec, ed, ee)
new_esEs22(xx3002, xx4002, app(app(app(ty_@3, ff), fg), fh)) → new_esEs12(xx3002, xx4002, ff, fg, fh)
new_esEs15(Nothing, Nothing, ce) → True
new_esEs5(xx301, xx401, ty_Bool) → new_esEs6(xx301, xx401)
new_esEs13(Left(xx3000), Left(xx4000), ty_@0, cb) → new_esEs16(xx3000, xx4000)
new_esEs27(xx3001, xx4001, ty_Float) → new_esEs17(xx3001, xx4001)
new_esEs27(xx3001, xx4001, app(ty_Maybe, bga)) → new_esEs15(xx3001, xx4001, bga)
new_esEs23(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs5(xx301, xx401, ty_Double) → new_esEs8(xx301, xx401)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs11(xx300, xx400)
new_esEs24(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs7(EQ, EQ) → True
new_esEs22(xx3002, xx4002, ty_Bool) → new_esEs6(xx3002, xx4002)
new_esEs23(xx3000, xx4000, ty_Ordering) → new_esEs7(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs6(True, True) → True
new_esEs27(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Float) → new_esEs17(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs10(:(xx3000, xx3001), :(xx4000, xx4001), be) → new_asAs(new_esEs23(xx3000, xx4000, be), new_esEs10(xx3001, xx4001, be))
new_esEs20(xx3000, xx4000, app(ty_Ratio, ea)) → new_esEs18(xx3000, xx4000, ea)
new_esEs13(Left(xx3000), Left(xx4000), ty_Int, cb) → new_esEs9(xx3000, xx4000)
new_esEs5(xx301, xx401, ty_@0) → new_esEs16(xx301, xx401)
new_esEs27(xx3001, xx4001, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs12(xx3001, xx4001, bfb, bfc, bfd)
new_esEs26(xx3000, xx4000, app(app(ty_@2, bee), bef)) → new_esEs14(xx3000, xx4000, bee, bef)
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs22(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs15(Just(xx3000), Just(xx4000), app(app(ty_@2, bha), bhb)) → new_esEs14(xx3000, xx4000, bha, bhb)
new_esEs13(Right(xx3000), Right(xx4000), ca, app(ty_[], baa)) → new_esEs10(xx3000, xx4000, baa)
new_esEs27(xx3001, xx4001, ty_Bool) → new_esEs6(xx3001, xx4001)
new_esEs7(EQ, GT) → False
new_esEs7(GT, EQ) → False
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs7(xx3000, xx4000)
new_esEs20(xx3000, xx4000, ty_Ordering) → new_esEs7(xx3000, xx4000)
new_sr(Neg(xx30000), Neg(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs20(xx3000, xx4000, ty_Integer) → new_esEs11(xx3000, xx4000)
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_@0) → new_esEs16(xx3000, xx4000)
new_sr(Pos(xx30000), Pos(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_asAs(False, xx42) → False
new_esEs23(xx3000, xx4000, ty_@0) → new_esEs16(xx3000, xx4000)
new_primEqNat0(Zero, Zero) → True
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Int) → new_esEs9(xx3000, xx4000)
new_primMulNat0(Zero, Succ(xx400000)) → Zero
new_primMulNat0(Succ(xx300000), Zero) → Zero
new_esEs15(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs15(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs7(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Bool) → new_esEs6(xx3001, xx4001)
new_esEs5(xx301, xx401, ty_Char) → new_esEs19(xx301, xx401)
new_esEs22(xx3002, xx4002, app(ty_[], fd)) → new_esEs10(xx3002, xx4002, fd)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs16(xx3000, xx4000)
new_esEs21(xx3001, xx4001, app(ty_Maybe, fb)) → new_esEs15(xx3001, xx4001, fb)
new_esEs27(xx3001, xx4001, ty_Ordering) → new_esEs7(xx3001, xx4001)
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Bool) → new_esEs6(xx3000, xx4000)
new_esEs5(xx301, xx401, app(ty_Maybe, bde)) → new_esEs15(xx301, xx401, bde)
new_esEs13(Right(xx3000), Right(xx4000), ca, app(ty_Maybe, bba)) → new_esEs15(xx3000, xx4000, bba)
new_esEs13(Left(xx3000), Left(xx4000), app(app(app(ty_@3, gh), ha), hb), cb) → new_esEs12(xx3000, xx4000, gh, ha, hb)
new_esEs13(Right(xx3000), Right(xx4000), ca, app(ty_Ratio, bbb)) → new_esEs18(xx3000, xx4000, bbb)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs6(xx300, xx400)
new_esEs4(xx300, xx400, app(app(app(ty_@3, bf), bg), bh)) → new_esEs12(xx300, xx400, bf, bg, bh)
new_esEs4(xx300, xx400, app(ty_Maybe, ce)) → new_esEs15(xx300, xx400, ce)
new_esEs5(xx301, xx401, app(app(ty_@2, bdc), bdd)) → new_esEs14(xx301, xx401, bdc, bdd)
new_esEs5(xx301, xx401, app(app(ty_Either, bda), bdb)) → new_esEs13(xx301, xx401, bda, bdb)
new_esEs16(@0, @0) → True
new_esEs5(xx301, xx401, ty_Int) → new_esEs9(xx301, xx401)
new_primPlusNat0(Succ(xx430), xx400000) → Succ(Succ(new_primPlusNat1(xx430, xx400000)))
new_esEs20(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs27(xx3001, xx4001, app(ty_[], bfa)) → new_esEs10(xx3001, xx4001, bfa)
new_esEs27(xx3001, xx4001, app(app(ty_@2, bfg), bfh)) → new_esEs14(xx3001, xx4001, bfg, bfh)
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs20(xx3000, xx4000, ty_Float) → new_esEs17(xx3000, xx4000)
new_esEs13(Right(xx3000), Left(xx4000), ca, cb) → False
new_esEs13(Left(xx3000), Right(xx4000), ca, cb) → False
new_esEs13(Right(xx3000), Right(xx4000), ca, app(app(ty_Either, bae), baf)) → new_esEs13(xx3000, xx4000, bae, baf)
new_esEs5(xx301, xx401, ty_Float) → new_esEs17(xx301, xx401)
new_esEs5(xx301, xx401, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs12(xx301, xx401, bcf, bcg, bch)
new_esEs4(xx300, xx400, ty_Double) → new_esEs8(xx300, xx400)
new_esEs15(Just(xx3000), Just(xx4000), app(ty_Maybe, bhc)) → new_esEs15(xx3000, xx4000, bhc)
new_primPlusNat1(Zero, Succ(xx4000000)) → Succ(xx4000000)
new_primPlusNat1(Succ(xx4300), Zero) → Succ(xx4300)
new_esEs14(@2(xx3000, xx3001), @2(xx4000, xx4001), cc, cd) → new_asAs(new_esEs26(xx3000, xx4000, cc), new_esEs27(xx3001, xx4001, cd))
new_esEs27(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs21(xx3001, xx4001, ty_@0) → new_esEs16(xx3001, xx4001)
new_esEs8(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs5(xx301, xx401, ty_Ordering) → new_esEs7(xx301, xx401)
new_esEs22(xx3002, xx4002, app(ty_Maybe, ge)) → new_esEs15(xx3002, xx4002, ge)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_Either, ca), cb)) → new_esEs13(xx300, xx400, ca, cb)
new_esEs20(xx3000, xx4000, app(ty_Maybe, dh)) → new_esEs15(xx3000, xx4000, dh)
new_esEs21(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs15(Just(xx3000), Just(xx4000), ty_@0) → new_esEs16(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Integer) → new_esEs11(xx3001, xx4001)
new_esEs5(xx301, xx401, ty_Integer) → new_esEs11(xx301, xx401)
new_esEs13(Left(xx3000), Left(xx4000), app(ty_Maybe, hg), cb) → new_esEs15(xx3000, xx4000, hg)
new_esEs18(:%(xx3000, xx3001), :%(xx4000, xx4001), cf) → new_asAs(new_esEs24(xx3000, xx4000, cf), new_esEs25(xx3001, xx4001, cf))
new_esEs7(EQ, LT) → False
new_esEs7(LT, EQ) → False
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Ordering) → new_esEs7(xx3000, xx4000)
new_esEs21(xx3001, xx4001, app(app(ty_Either, ef), eg)) → new_esEs13(xx3001, xx4001, ef, eg)
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Double) → new_esEs8(xx3000, xx4000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(xx3001, xx4001, ty_Float) → new_esEs17(xx3001, xx4001)
new_asAs(True, xx42) → xx42
new_esEs10([], :(xx4000, xx4001), be) → False
new_esEs10(:(xx3000, xx3001), [], be) → False
new_primMulNat0(Succ(xx300000), Succ(xx400000)) → new_primPlusNat0(new_primMulNat0(xx300000, Succ(xx400000)), xx400000)
new_esEs15(Nothing, Just(xx4000), ce) → False
new_esEs15(Just(xx3000), Nothing, ce) → False
new_esEs27(xx3001, xx4001, ty_Integer) → new_esEs11(xx3001, xx4001)
new_esEs22(xx3002, xx4002, ty_Double) → new_esEs8(xx3002, xx4002)
new_esEs23(xx3000, xx4000, ty_Bool) → new_esEs6(xx3000, xx4000)
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs13(Left(xx3000), Left(xx4000), ty_Float, cb) → new_esEs17(xx3000, xx4000)
new_esEs13(Left(xx3000), Left(xx4000), ty_Integer, cb) → new_esEs11(xx3000, xx4000)
new_esEs6(True, False) → False
new_esEs6(False, True) → False
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs13(Right(xx3000), Right(xx4000), ca, app(app(app(ty_@3, bab), bac), bad)) → new_esEs12(xx3000, xx4000, bab, bac, bad)
new_esEs10([], [], be) → True
new_esEs6(False, False) → True
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs11(xx3000, xx4000)
new_esEs9(xx300, xx400) → new_primEqInt(xx300, xx400)
new_esEs13(Right(xx3000), Right(xx4000), ca, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Int) → new_esEs9(xx300, xx400)
new_esEs23(xx3000, xx4000, app(app(ty_@2, bca), bcb)) → new_esEs14(xx3000, xx4000, bca, bcb)
new_esEs7(GT, GT) → True
new_esEs13(Left(xx3000), Left(xx4000), app(ty_[], gg), cb) → new_esEs10(xx3000, xx4000, gg)
new_esEs4(xx300, xx400, app(app(ty_@2, cc), cd)) → new_esEs14(xx300, xx400, cc, cd)
new_esEs21(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_esEs26(xx3000, xx4000, app(app(ty_Either, bec), bed)) → new_esEs13(xx3000, xx4000, bec, bed)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(xx3001, xx4001, app(ty_Ratio, fc)) → new_esEs18(xx3001, xx4001, fc)
new_esEs15(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bgd), bge), bgf)) → new_esEs12(xx3000, xx4000, bgd, bge, bgf)
new_esEs13(Left(xx3000), Left(xx4000), app(ty_Ratio, hh), cb) → new_esEs18(xx3000, xx4000, hh)

The set Q consists of the following terms:

new_esEs23(x0, x1, ty_Bool)
new_esEs15(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_@0)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(LT, EQ)
new_esEs7(EQ, LT)
new_esEs9(x0, x1)
new_esEs20(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10([], [], x0)
new_esEs11(Integer(x0), Integer(x1))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_@0)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_esEs15(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs15(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs15(Just(x0), Nothing, x1)
new_esEs27(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(LT, LT)
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs15(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs7(GT, LT)
new_esEs7(LT, GT)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Integer)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Double)
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Int)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Succ(x0))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs10(:(x0, x1), [], x2)
new_esEs26(x0, x1, ty_@0)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs21(x0, x1, ty_Double)
new_esEs27(x0, x1, ty_Ordering)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(@0, @0)
new_asAs(True, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_primPlusNat0(Zero, x0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_esEs19(Char(x0), Char(x1))
new_esEs5(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Bool)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Nothing, Nothing, x0)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs20(x0, x1, ty_@0)
new_esEs15(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Double)
new_esEs7(GT, GT)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs4(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs15(Just(x0), Just(x1), ty_@0)
new_esEs6(False, False)
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Ordering)
new_esEs22(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10([], :(x0, x1), x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs27(x0, x1, ty_Float)
new_esEs4(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Integer)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs4(x0, x1, ty_Char)
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Int)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs15(Just(x0), Just(x1), app(ty_[], x2))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Ordering)
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs7(GT, EQ)
new_esEs7(EQ, GT)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs27(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Int)
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs15(Just(x0), Just(x1), ty_Char)
new_esEs15(Just(x0), Just(x1), ty_Int)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs15(Nothing, Just(x0), x1)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs5(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs5(x0, x1, ty_Integer)
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Int)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs5(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs5(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_sr(Pos(x0), Pos(x1))
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat1(Zero, Zero)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Char)
new_asAs(False, x0)
new_esEs6(True, True)
new_esEs15(Just(x0), Just(x1), ty_Double)
new_esEs5(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), ty_Integer)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(EQ, EQ)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(Just(x0), Just(x1), ty_Ordering)
new_esEs6(True, False)
new_esEs6(False, True)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Float)
new_esEs5(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs23(x0, x1, ty_Float)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs27(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xx4, :(xx30, xx31), ba, bb) → new_foldr(xx4, xx31, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: